@$i$: with declarations ds:${\it ds}$ da:${\it da}$($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$)$\rightarrow$ with declarations ds:${\it ds}$da:${\it da}$ else  fi